%explain section
In this section, we provide a catalog of bad smells in contracts that result from DBC development. As we tried to show in the example, smells are not necessarily hazardous, but they show evidence about possible errors and hard-to-change programs.
%explain catalog format - taken from refactoring workbook
For a more concise and uniform explanation of bad smells and to ease their identification, we adopted a specific format for smell descriptions. The format used for our catalog are inspired by code smells from Wake's book~\cite{refact-workbook} on refactoring. Smells are described with the following properties:
\begin{itemize}
  \item \textbf{Brief Description.} Description emphasizing the problems behind the smell;
	\item \textbf{Symptoms.} Clear signs of the described bad smells in contracts and code;
	\item \textbf{Example.} Example of the bad smell, using the system described in Section~\ref{sect:motivatingExample};
	\item \textbf{Causes.} Likely ways of having this smell present in the program;
	\item \textbf{What to do.} Although this is not the focus in this paper, ideas on how to refactor the program for eliminating or minimizing the impact of the smell;
	\item \textbf{Example Solution.} A possible refactored program;
	\item \textbf{Payoff.} Advantages in avoiding this smells, in terms of general quality in DBC development;
	\item \textbf{Contraindications.} Situation in which removing the smell may not be desirable. 
\end{itemize}

%jml
We focused on JML as the contract language, thus smells are in principle specific to particular JML constructs. Still, they are likely to appear in similar constructs from in other contract languages (JML, Eiffel, Spec\#~\cite{spec-sharp-reference}, among others). In this paper, we only describe some smells in detail; the complete set of DBC smells that we catalogued so far are presented in Table~\ref{tab:smells}.
We describe six (6) smells in detail: \emph{Open Doors}, \emph{Field Obsession}, \emph{Illogical Contracts}, \emph{Complexity Magnetism}, \emph{Long Specs} and \emph{Specification Overkill}.\\

\subsection{Bad Smell: Open Doors}
\label{smell:open}
\noindent\textbf{Brief Description.} Contracts that expose private data, threatening encapsulation.\\

\noindent\textbf{Symptoms.} Indication is given with direct access to private or protected fields (or methods) in public contracts. In JML, it is explicited with the \code{spec\_public} or \code{spec\_protected} modifiers. The \code{\textbf{forall}} operator represents an universal quantifier, with three components (separated by semicolons): variable declaration, variable delimitation and boolean expression with the predicate.\\

\noindent\textbf{Example.}
\begin{lstlisting}[frame=single,framerule=0pt,numbers=none]
public class Document {
	private /*@ spec_public @*/ Document[] versions;
	/*@ invariant(
	  @	 \forall int i; 0<=i && i<versions.length; 
	  @		  versions[i].getAuthor().equals(
	  @														getAuthor())
	  @	); 
	  @*/
..}
\end{lstlisting}

\noindent\textbf{Causes.} Developers need a way to specify which components of internal data must be modified in method contracts or invariants that have visibility that is less retricted than data. Also, this can be caused by lack of abstraction when specifying methods.\\

\noindent\textbf{What to do.} In cases which fields must be used to indicate state changes and contracts, a model field can be created, representing the hidden concrete field; the contracts then must be changed to use the model field, replacing accesses to concrete field. However, if many fields are used in contracts, developers should consider using query methods instead (see bad smell~\ref{smell:field}). Regarding methods, model methods can be used, in which code delegates the call to concrete methods.

\noindent\textbf{Solution to the example.}

\begin{lstlisting}[frame=single,framerule=0pt,numbers=none]
public class Document {
	/*@ public model JMLEqualsSet versionsSet;
	  @ invariant( 
	  @  \forall int i; 0<=i && i<versionsSet.size; 
	  @		  ((Document)versionsSet.itemAt(i)).
	  @			 	  getAuthor().equals(getAuthor())
	  @	); 
	  @*/
..}
\end{lstlisting}

\noindent\textbf{Payoff.} Encapsulation is promoted, even in the presence of contracts. Removing this smell tends to bring abstraction to contracts, which is highly desirable in DBC.\\

\noindent\textbf{Contraindications.} Excess of model fields tend to raise complexity of contracts. In this case, query methods should be a better option. In some fields, however, query methods are not possibly used -- from some encapsulation requirement in the application. In this case, the contracts should be revised, as possibly they could not expose these particular fields.
 
\subsection{Bad Smell: Field Obsession}
\label{smell:field}
\noindent\textbf{Brief Description.} There is an excessive number of direct field accesses in contracts, making these contracts more sensitive to changes in internal data.\\

\noindent\textbf{Symptoms.} Excess of direct access to several fields from a class in contracts.\\

\noindent\textbf{Example.} For the \code{setSections} method, the contract includes pre and postconditions, it includes the JML \code{\textbf{assignable}} clause, that indicate frame conditions (variables that may possibly be assigned values). The invariant refers to fields \code{n} and \code{sections}.
\begin{lstlisting}[frame=single,framerule=0pt,numbers=none]
public class Document { ..
	//@ public invariant 0<=n && n<sections.length;

	/*@ assignable sections,n;
	  @ ensures n == secs.length
	  @ ensures( 
	  @	  \forall int i; 0<=i && i<n; 
	  @		   sections[i] == secs[i]
	  @ );
    @*/ 
	public void setSections(Section[] secs){..}
..}
\end{lstlisting}

\noindent\textbf{Causes.} In general, this smell happens when developers avoid using methods, maybe fearing long specifications. This can also happen regardless of concrete or model fields.\\

\noindent\textbf{What to do.} Mainly solutions must include the use of query (accessor) methods. In Eiffel, for instance, field accesses automatically behave as query methods -- JML does not offer this feature, since it would demand changes in the semantics of the programming language (Java).\\

\noindent\textbf{Solution to the example.}

\begin{lstlisting}[frame=single,framerule=0pt,numbers=none]
public class Document { ..
	//@ public invariant 0<=getSectionsSize() &&
  //@   getSectionsSize()<sections.length;

	/*@ assignable sections, n;
	  @ ensures getSectionsSize() == secs.length;
	  @ ensures (\forall int i;
	  @ 				0<=i && i<getSectionsSize();
    @    			getItemFromSections(i)==secs[i]);
    @*/ 
	public void setSections(Section[] secs){..}
..}
\end{lstlisting}

\noindent\textbf{Payoff.} Besides adding abstraction to contracts, this solution usually makes the contract easier to understand.\\

\noindent\textbf{Contraindications.} The contract can get considerably long, if too many fields are accessed. In this scenario, contracts can be rewritten with improvements, by using auxiliary model methods (see Bad Smell~\ref{smell:illogical}).\\

\subsection{Bad Smell: Illogical Contracts}
\label{smell:illogical}
\noindent\textbf{Brief Description.} Contracts defining predicates with logics that gets too hard too understand.\\

\noindent\textbf{Symptoms.} Long boolean predicates within contracts, for instance in the same \code{\textbf{invariant}} clause. The contract tends to be hard to write or understand.\\

\noindent\textbf{Example.} In the \code{Document} class, there may be invariant stating that the sections for older versions of a document must be present in the later versions. In JML, this must be written as two universal quantifications.
\begin{lstlisting}[frame=single,framerule=0pt,numbers=none]
public class Document { ..
/*@ invariant(
  @	 \forall int i; 0<=i && i<versionsSet.size;
  @   (\forall int j; 0<=j && j<sectionsSet.size;
  @    				((Document)versionsSet.
  @    				itemAt(i)).sectionsSet.
  @    				has(sectionsSet.itemAt(j)))
  @ );  
  @*/
..}	
\end{lstlisting}

\noindent\textbf{Causes.} Some complex specifications may be required; it might be more common to JML as it follows Java syntax with extensions, which surely make boolean predicates verbose. Abstraction in this scenario is a challenge.\\

\noindent\textbf{What to do.} Declaration of JML-pure boolean methods that represent predicates. In JML, \emph{pure methods} are required to have no side effects. The methods are used in contracts as auxiliary predicates. In this context, naming is important, in order to improve readability.\\

\noindent\textbf{Solution to the example.} In JML, auxiliary predicates can be declares as model methods.

\begin{lstlisting}[frame=single,framerule=0pt,numbers=none]
public class Document{ ..
	/*@ invariant(
	  @	 \forall int i; 0<=i && i<versionsSet.size;
    @    hasAllOldVersionSections(versionsSet.
    @    					itemAt(i)
    @ );
	  @ public model pure boolean 
	  @   hasAllOldVersionSections(Document d){
	  @ 	  return d.sectionsSet.has(
	  @       getBaseDocumentSections());
	  @ }
	  @
	  @ public model pure JMLEqualsSet 
	  @   getBaseDocumentSections(){
	  @  	  return this.sectionsSet;
	  @ }  
	  @*/
..}	
\end{lstlisting}

\noindent\textbf{Payoff.} The solution helps raising abstraction in contracts, making them easier to read and to edit.\\

\noindent\textbf{Contraindications.} In some situations, there may be necessary to create too many methods, which can make the specification longer than the original. Therefore, it is sensible to revise the contracts, in order to find better ways to rewrite complex statements (which is not always possible). In addition, if predicates become substantially complex due to the application domain, separation and comments in natural language can be used, especially if the contracts will not be subject to tool-assisted verification. For instance, JML allows predicates in natural language, although they are not considered for reasoning.\\

\subsection{Bad Smell: Complexity Magnetism}
\label{smell:complexity}
\noindent\textbf{Brief Description.} Model fields with complex definitions in \code{\textbf{represents}} clauses.\\

\noindent\textbf{Symptoms.} When using abstract model fields, the \code{\textbf{represents}} clause may become very complex; this scenario hinders readability and maintainability, especifically for class implementers (clients should not have access to \code{\textbf{represents}}. \\

\noindent\textbf{Example.} In this case, \code{versionsSet} model field has a complex definition, which is encapsulated in a model method. This method copies each element of the concrete \code{ArrayList} to the abstract set. \begin{lstlisting}[frame=single,framerule=0pt,numbers=none]
public class Document { ..
	//@ public model JMLEqualsSet versionsSet;
	
	//@ private represents versionsSet <- 
  //@    abstractVersions();
	
	/*@ private model pure JMLEqualsSet 
	  @   abstractVersions() {
		@ 	  JMLEqualsSet ret = new JMLEqualsSet();
		@    	Iterator it = versions.iterator();
		@ 	  while (it.hasNext()) {
		@ 		  ret.insert(it.next());
		@   	}
		@ 	  return ret; }
	  @*/
..}
\end{lstlisting}

\noindent\textbf{Causes.} This situation arises depending on how hard it is to abstract from concrete data. Also, complexity of specific data structures is critical (for example, collection manipulation from Java).\\

\noindent\textbf{What to do.} For simple collections, the JML model API offers methods like \code{convertFrom}; the mathematical toolkit of the language should support this solution. In cases that result in complex model methods that abstract away details from internal data, other auxiliary methods can be extracted (analogous to the Extract Method refactoring~\cite{refact-book}).\\

\noindent\textbf{Solution to the example.}

\begin{lstlisting}[frame=single,framerule=0pt,numbers=none]
public class Document{ ..	
	//@ public model JMLEqualsSet versionsSet;
	
	//@ private represents versionsSet <- 
  //@    JMLEqualsSet.convertFrom(getVersions());
..}
\end{lstlisting}

\noindent\textbf{Payoff.} Contracts become easier to write and understand by implementers. Abstraction in general is higher. Despite this example, a variation of this smell can happen in the opposite sitation: an one-line definition of \code{\textbf{represents}} can get too complex; in this case, the model method should be included.\\

%\noindent\textbf{Contraindications.}  

\subsection{Bad Smell: Long Specs}
\label{smell:long}
\noindent\textbf{Brief Description.} Unnecessary heavyweight style in DBC applications, covering every possible behavior for methods.\\

\noindent\textbf{Symptoms.} In JML, developers may use two styles of contracts (specification cases): heavyweight or lightweight. For the first style, differently from the latter, JML expects that developers only omit parts of the specification when the default is appropriate, specifying behavior completely. It is indicated by clauses \code{\textbf{normal\_behavior}} and \code{\textbf{exceptional\_behavior}}. Excess of heavyweight contracts obstructs good DBC development, losing abstraction and readability.\\

\noindent\textbf{Example.} In the contract, the \code{also} keyword indicates complementarity of specification cases. The \code{\textbf{signals\_only}} and \code{\textbf{signals}} constructs define the Java exceptions possibly thrown by the method in exceptional behavior.
\begin{lstlisting}[frame=single,framerule=0pt,numbers=none]
public class Document { ..
/*@ public normal_behavior
	@ 	requires s.getAuthor().equals(a) && 
  @            !s.isLocked();
	@ 	assignable s;
	@ 	ensures s.isLocked();
	@ also
	@ public exceptional_behavior
	@ 	requires s.isLocked();
	@ 	assignable nothing;
	@ 	signals_only Exception;
	@ 	signals (SectionLockedException e);
	@*/
	public void editSection(Section s, Author a) throws SectionLockedException {..}
..}
\end{lstlisting}

\noindent\textbf{Causes.} Sometimes it is required that specifications get replicated, with the intention of specifying complex contracts. Also, developers may wish to document every situation in which exceptions are thrown.\\

\noindent\textbf{What to do.} In DBC, lightweight contracts are much more desirable, as both clients and implementers should often refer to contracts as documentation. In this scenario, exceptional behaviors should be removed, omiting exceptional situations that are not relevant for implementing the program. Also, the \code{normal\_behavior} clause can be removed.\\

\noindent\textbf{Solution to the example.}

\begin{lstlisting}[frame=single,framerule=0pt,numbers=none]
public class Document { ..
	
	/*@ requires s.getAuthor().equals(a) && 
    @          !s.isLocked();
		@ assignable s;
		@ ensures s.isLocked();
	  @ signals (SectionLockedException e);
	  @*/
	public void editSection(Section s, Author a) 
		throws SectionLockedException {..}
..}
\end{lstlisting}

\noindent\textbf{Payoff.} More importantly, better readability and maintainability of contracts. In avoiding heavyweight specifications in DBC, another benefit comes up: developers eliminate the risk of introducing specification mistakes by accidently defining overlapping specification cases (sobreposition of preconditions that does not make clear which one is valid for a given state).\\

\noindent\textbf{Contraindications.} When JML is applied in complete tool-assisted verification or test-case generation, to cover all specification cases is critical. In this scenario, certainly this is not considered a bad smell.\\

\subsection{Bad Smell: Specification Overkill}
\label{smell:specOver}
\noindent\textbf{Brief Description.} Excess of redundant specifications.\\

\noindent\textbf{Symptoms.} Repeated use of redundant clauses, such as  \code{\textbf{ensures\_redundantly}} or \code{\textbf{requires\_redundantly}}, which means that the contract was already valid in the given context, usually for documentation purposes; even different predicates with the same semantic are allowed.\\

\noindent\textbf{Example.} .
\begin{lstlisting}[frame=single,framerule=0pt,numbers=none]
public class Document {
  /*@ assignable versionsSet;
  	@ requires v != null;
  	@ ensures versionsSet.has(v); 
  	@ ensures_redundantly
  	@		(\exists  
  	@			int i; 0<=i && i<versionsSet.size;
  	@			  versionsSet.itemAt[i] == v);
		@*/
  public void addVersion(Version v){..}
..}
\end{lstlisting}

\noindent\textbf{Causes.} This bad smell may appear caused by needs for repeating specifications with the intention of explaining something complex. But, in other contexts, this can expose lack of attention to the existing predicates.\\

\noindent\textbf{What to do.} Mostly, redundant clauses can be removed, because that redundancy might shows the existence of unnecessary specification. In some cases only a good revision of predicates is enough. Also, it is better to use the simplest forms of the specifications, because  if it is possible to re-explain something simpler it is ever best use this simpler in a single turn.\\

\noindent\textbf{Solution to the example.}

\begin{lstlisting}[frame=single,framerule=0pt,numbers=none]
public class Document {
  /*@ assignable versionsSet;
    @ requires v != null;
    @ ensures versionsSet.has(v); 
    @*/
  public void addVersion(Version v) {..}
..}
\end{lstlisting}

\noindent\textbf{Payoff.} The specification becomes more clear and easily understood. Inconsistencies are avoided as redundancy is removed.\\

\noindent\textbf{Contraindications.} In a number of situations, the use of \code{\textbf{ensures\_redundantly}} is justified as a good way to explain complex contracts. In these cases it is important to look for ways to leave contracts in their simplest form possible. There is still the alternative of removing Smell~\ref{smell:illogical}.\\

\subsection{Other DBC Smells}

The complete catalog is showed in Table~\ref{tab:smells}. For instance, public methods with no specifications may be a suggestion of omission, or even unnecessary methods (\emph{Forgotten Boys}); duplicate contracts in methods can be better specified as invariants (\emph{Broken Record}). Further, developers tend to use Java collections in model fields declarations that represent mathematical sets; for better abstraction, the JML model API is more indicated (\emph{Math Horror}). Also, excess of helper methods -- methods that are not obliged to maintain contracts -- is a rich source of encapsulation problems (\emph{Unhelpful Helper}). 

%(overview of other smells) - table
\begin{table*}[ht]
\caption{Catalog of DBC Smells}
\begin{center}
\scalebox{0.8}{
\begin{tabular}{|l|l|}
\hline
\textbf{NAME} & \textbf{BRIEF DESCRIPTION} \\ \hline 
\textit{Open Doors} & \parbox{5.5cm}{contracts that expose private data} \\ \hline 
\textit{Field Obsession} & \parbox{5.5cm}{many direct accesses to variables in contracts} \\ \hline
\textit{Illogical Contracts} & \parbox{5.5cm}{contracts with logics that gets too hard too understand} \\ \hline 
\emph{Complexity Magnetism} & \parbox{5.5cm}{complex definition of model fields} \\ \hline 
\emph{Long Specs} & \parbox{5.5cm}{unnecessary heavyweight style} \\ \hline 
\emph{Specification Overkill} & \parbox{5.5cm}{excess of redundant specifications} \\ \hline 
\emph{Hollow Obssession} & \parbox{5.5cm}{repeated tests about null variable in contracts} \\ \hline
\emph{Forgotten Boys} & \parbox{5.5cm}{public methods lacking contracts} \\ \hline 
\emph{Broken Record} & \parbox{5.5cm}{duplication of constraints in method contracts} \\ \hline 
\emph{Private Contracts} & \parbox{5.5cm}{public contracts over private methods} \\ \hline
\emph{Math Horror} & \parbox{5.5cm}{use of Java collections to represent mathematical sets} \\ \hline 
\emph{Unhelpful Helper} & \parbox{5.5cm}{excess of helper methods} \\ \hline 
\emph{Same of the same} & \parbox{5.5cm}{repetition of contracts in subtypes} \\ \hline 
\emph{Construction Details} & \parbox{5.5cm}{repetition of postconditions in class constructors} \\ \hline 
\emph{Purely Nothing} & \parbox{5.5cm}{non-pure methods that have no assignable clause} \\ \hline
\emph{Exceptional Lapse} & \parbox{5.5cm}{exceptional behavior case lacking a specific exception thrown by the method}\\ \hline
\end{tabular}}
\label{tab:smells}
\end{center}
\end{table*}